T:Type, as,bs:(T List).
no_repeats(T; as)
 no_repeats(T; bs)
 ((as = bs)
  ((x:T. (x  as)  (x  bs))
   (x,y:T. l_before(x; y; as; T)  l_before(x; y; bs; T)))) 

latex

Definitions

x:A. B(x), t  T, l_before(x; y; l; T), (x  l), Type, no_repeats(T; l), P  Q, x:AB(x), prop{i:l}, x:A  B(x), P  Q, P  Q, P  Q, type List, s = t, cons(car; cdr), [], tl(l), n - m, if a<b then c else d, i <z j, b, i z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), hd(l), l[i], n + m, rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, ||as||, a < b, A, A  B, , {x:A| B(x)} , , False, guard(T), P  Q, left + right, x. t(x), True, T

Lemmas

squash wf, true wf, l before member2, l before member, no repeats cons, all functionality wrt iff, iff functionality wrt iff, cons before, cons member, nil member, iff wf, no repeats wf, l member wf, l before wf